Monoids as one-object categories, or not?

Iceland_jack 2020-05-07

{-# Language DataKinds                #-}
{-# Language DerivingVia              #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language PolyKinds                #-}
{-# Language RankNTypes               #-}
{-# Language RoleAnnotations          #-}
{-# Language StandaloneKindSignatures #-}

import Control.Category (Category(..))
import Data.Kind        (Type, Constraint)
import Data.Monoid      (Sum(..))

Every Monoid can be viewed as a Category. First of all monoids are “untyped”, there is no wrong way to compose a monoid m

(<>) :: m -> m -> m

but for a category cat we are more particular about our composition. I use (>>>) to highlight the “left-to-right” nature of the composition

(>>>) :: cat a b -> cat b c -> cat a c

This says

If you can get from a to b and from b to c; you can get from a to c.

one         :: a -> b
two         ::      b -> c
one >>> two :: a ------> c

For m to be typed it must have a source and a target. We really need to wrap it in a type with two phantom type parameters. But of what kind?

The standard answer in category theory is to define a category for a monoid that has a single object. “Dummy”, the unit ().

type OneObject :: Type -> () -> () -> Type
data OneObject m unit1 unit2 where
  OneObject :: m -> OneObject m '() '()

Since the source and target always have the same kind in a category I define the kind “Cat ob" for categories with objects of kind ob.

type Cat :: Type -> Type
type Cat ob = (ob -> ob -> Type)

type OneObject :: Type -> Cat ()

As an example, our regular function arrow (->) :: Cat Type has types as objects.

This means we turn our old monoid "hi" into something with a source '() :: () and target '() :: ()

OneObject "hi" :: OneObject String '() '()

But there is a problem. We cannot make it a Category. Actually, we fatally cannot make it a newtype either but first thing's first: Why can't it be a category?

instance Monoid m => Category (OneObject m) where
  id :: OneObject m unit unit
  id = undefined

  (.) :: OneObject m unit2 unit3
      -> OneObject m unit1 unit2
      -> OneObject m unit1 unit3
  OneObject m . OneObject m' =
    OneObject (m <> m')

Everything crumbles as we attempt to define id. There is only one inhabitant of () so there is no surprise that we chose the source and target to be '()

OneObject :: m -> OneObject m '() '()

but GHC doesn't know that.. If even if we partially define id = OneObject undefined .. ghc shrieks back:

  Expected type: OneObject m unit unit
    Actual type: OneObject m '() '()

But what if we changed OneObject to return OneObject m unit unit instead? In a way ghc suggests this,

type OneObject :: Type -> Cat ()
data OneObject m unit1 unit2 where
  OneObject :: m
            -> OneObject m unit unit

Our source and target are always the same, and this in fact allows us to define a Category instance.

instance Monoid m => Category (OneObject m) where
  id :: OneObject m unit unit
  id = OneObject mempty
  
  (.) :: OneObject m unit2 unit3
      -> OneObject m unit1 unit2
      -> OneObject m unit1 unit3
  OneObject m . OneObject m =
    OneObject (m <> m')

This is good. You can almost make out the core idea

id  = mempty
(.) = (<>)

But why can't we make it a newtype? Because requiring that unit1 and unit2 be the same is equivalent to writing a context with an equality constraint

-- error: A newtype constructor cannot have a context in its type
type    OneObject :: Type -> Cat ()
newtype OneObject m unit1 unit2 where
  OneObject :: unit1 ~ unit2
            => m
            -> OneObject m unit1 unit2

It took me a while to let go of the mindset that the two objects had to match. Did they really? If there is only one object () then maybe it doesn't matter if we vary the objects.

type role
     OneObject representational phantom phantom

type    OneObject :: Type -> Cat ()
newtype OneObject m unit1 unit2 where
  OneObject :: m -> OneObject m unit1 unit2

In addition our roles are now exactly how we want them. First argument can be coerced if the monoid can be coerced. The last two arguments can be coerced to anything because they are phantom types.

We see this by instantiating coerce (in ghci for example) at OneObject _ _ _
and  seeing that each argument can be coerced but only the first argument gets a coercible constraint

> coerce @(OneObject _ _ _) @(OneObject _ _ _)
coerce @(OneObject _ _ _) @(OneObject _ _ _)
  :: Coercible m m'
  => OneObject m  unit  unit2
  -> OneObject m' unit' unit2'

The category instance still compiled. Good. It's worth noting that the core idea can be expressed better now with type applications and coerce from Data.Coerce

  id  = coerce do mempty @m
  (.) = coerce do (<>)   @m

Maybe the object kind () is restrictive as well. Was I following the letter of the law too carefully when I insisted that there only be a single object.

I carefully made my category construction polykinded.

type OneObject :: Type -> forall ob. Cat ob

Nothing else changes although now I need a better name for this category.

Now we can derive other categories from it

type    SumCat :: forall ob. Cat ob
newtype SumCat dummy dummy' = SumCat Int
  deriving Category
  via OneObject (Sum Int) @ob

So yeah, what should OneObject be called and are there objections to adding it to Control.Category?

reddit: https://www.reddit.com/r/haskell/comments/gf54o6/monoids_as_oneobject_categories_or_not/

patreon: https://www.patreon.com/Iceland_jack